Danny Amor's Online Library/Danny Amor's Online Library - Volume 1.iso/html/faqs/faq/z-faq

Text File | 1995-07-25 | 23.7 KB | 427 lines

Subject: comp.specification.z Frequently Asked Questions (Monthly)
Newsgroups: comp.specification.z,news.answers,comp.answers
From: [e-mail]
Date: Tue, 1 Nov 1994 02:00:04 GMT

Archive-name: z-faq
Last-modified: 19 October 1994
Maintainer: Jonathan Bowen <[e-mail]>                           |
URL: file://ftp.comlab.ox.ac.uk/pub/Zforum/faq                               |


NAME:     comp.specification.z
STATUS:   unmoderated
PURPOSE:  Discussion concerning the formal specification notation Z.

(If you have read this before, changed and new sections since the
previously issued version are marked with `|' in the right hand margin.)

Note: nearly all UK telephone numbers will have a "1" prefixed to them       |
in future. Currently there is a changeover period in operation. The UK       |
contact telephone numbers have been updated en masse in this message.        |
If there are any mistakes, please contact the email address at the end       |
of the message. Thank you.                                                   |

Questions have been marked with "Subject:" at the start of the line to
allow some newsreaders to scan them easily (e.g., "^G" within "rn").
This FAQ message is available on-line on the World Wide Wed (WWW) hypertext
http://www.cis.ohio-state.edu/hypertext/faq/usenet/z-faq/faq.html page
where it is split into convenient sections.

Subject: What is it?

The comp.specification.z electronic USENET newsgroup was established in
June 1991 and is intended to handle messages concerned with the formal
specification notation Z (pronounced `zed'). It has an estimated
readership of around 45,000 people worldwide.  Z, based on set theory
and first order predicate logic, has been developed at the Programming
Research Group (PRG) at the Oxford University Computing Laboratory and
elsewhere since the late 1970s.  It is now used by industry as part          |
of the software (and hardware) development process in both the UK and
the US. It is currently undergoing international ISO standardization.        |
Comp.specification.z provides a convenient forum for messages concerned
with recent developments and the use of Z.  Pointers to and reviews of
recent books and articles are particularly encouraged. These will be
included in the Z bibliography (see below) if they appear in
comp.specification.z.

Subject: What if I know someone interested without access to USENET news?

There is an associated Z FORUM electronic mailing list that was
initiated in January 1986 by Ruaridh Macdonald, RSRE, UK.  Articles are
now automatically cross-posted between comp.specification.z and the
mailing list for those whose do not have access to USENET news.  This
may apply especially to industrial Z users who are particularly
encouraged to subscribe and post their experiences to the list.  Please
contact <[e-mail]> with your name, address and
email address to join the mailing list (or if you change your email
address or wish to be removed from the list). Readers are strongly
urged to read the comp.specification.z newsgroup rather than the Z
FORUM mailing list if possible. Messages for submission to the Z FORUM
mailing list and the comp.specification.z newsgroup may be emailed to
<[e-mail]>.  This method of posting is particularly
recommended for important messages like announcements of meetings since
not all messages posted on comp.specification.z reach the PRG.
  A mailing list for the Z User Meeting educational issues session has
been set by Neville Dean, Anglia Polytechnic University, UK.  Anyone
interested may join by emailing <[e-mail]> with
your contact details.
  A specialist electronic mailing for discussion of SAZ, a combination
of the structured method SSADM and Z also exists.  To join, contact
<[e-mail]>.

Subject: What if I know someone interested without access to email?

If you wish to join the postal Z mailing list, please send your address
to Amanda Kingscote, Praxis plc, 20 Manvers Street, Bath BA1 1PX,
UK  (tel [phone], fax [phone], email <[e-mail]>).
This will ensure you receive details of Z meetings, etc., particularly
for people without access to electronic mail.

Subject: How can I join in?

If you are currently using Z, you are welcome to introduce yourself to
the newsgroup and Z FORUM list by describing your work with Z or
raising any questions you might have about Z which are not answered
here. You may also advertize publications concerning Z which you or
your colleagues produce. These may then be added to the master Z
bibliography maintained at the PRG (see below).

Subject: Where are Z-related files archived?

There is an automatic electronic mail-based electronic archive server
at the PRG which contains most messages and back-issues on
comp.specification.z and Z FORUM, as well as a selection of other
Z-related files.  Send an email message containing the command "help"
to <[e-mail]> for further information on how to
use the server. A command of "index z" will list the Z-related files.
If you have serious trouble accessing the archive server, please
contact the address <[e-mail]>.
  The archive is also available via anonymous FTP on the Internet
under the ftp.comlab.ox.ac.uk:/pub/Zforum directory. Type the
command "ftp ftp.comlab.ox.ac.uk" (or alternatively "ftp 163.1.27.2"
if this does not work) and use "anonymous" as the login id and your
email address as the password when prompted. The FTP command
"cd pub/Zforum" will get you into the Z archive directory.  The file
ftp.comlab.ox.ac.uk:/pub/Zforum/README gives some general information
and ftp.comlab.ox.ac.uk:/pub/Zforum/00index gives a list of the
files.  (Retrieve these using the FTP command "get README", for
example.)
  Information on the World Wide Web (WWW) is available on the
http://www.comlab.ox.ac.uk/archive/zforum.html page.  See also the
http://www.comlab.ox.ac.uk/archive/formal-methods.html page on formal
methods in general. The WWW global hypertext system is accessible using
the "mosaic" or "lynx" programs for example. Contact your system
manager if WWW access is not available on your system.

Subject: What tools are available?

Various tools for formatting, type-checking and aiding proofs in Z are
available.  A free LaTeX style file and documentation can be obtained
from the PRG archive server. To receive this via email, send a message
containing the command "send z zed.sty zguide.tex" to the PRG archive
server (or access the ftp.comlab.ox.ac.uk:/pub/Zforum/zed.sty and
ftp.comlab.ox.ac.uk:/pub/Zforum/zguide.sty files). A newer style
"csp_zed.sty" is available in the same location, which uses the new
font selection scheme and covers CSP and Z symbols. A style for
Object-Z "oz.sty" with a guide "oz.tex" is also accessible.
  The fuzz package, a syntax and type checker with a LaTeX style option
and fonts, is available from J.M. Spivey Computing Science Consultancy,
34, Westlands Grove, Stockton Lane, York YO2 0EF, UK. It is compatible
with the second edition of Spivey's Z Reference Manual (see below).
Contact Mike Spivey (email <[e-mail]>) for
further information. Alternatively send the command "send z fuzz" to
the PRG archive server or access ftp.comlab.ox.ac.uk:/pub/Zforum/fuzz
for brief information and an order form.
  CADiZ, a Unix-based suite of tools for checking and typesetting Z
specifications.  CADiZ also supports previewing and interactive
investigation of specifications.  It is available from York Software
Engineering, University of York, York YO1 5DD, UK (tel [phone],
fax [phone]). CADiZ supports a language like that of the Z Base
Standard (Version 1.0). A particular extension allows one specification
document to import another, including the mathematical toolkit as one
such document. Typesetting Support is available for both troff and for
LaTeX. Browsing operations include display of information deduced by
the type-checker (e.g. types of expressions and uses of variables),
expansion of schemas, pre- and post-condition calculation, and
simplification by the one-point rule.  Currently work is on-going to
provide support for refinement of Z specifications to Ada programs
through a literate program development method and integrated proof
facilities.  Further information is available from David Jordan at York
on <[e-mail]>.
  ProofPower is a suite of tools supporting specification and proof in
Higher-Order Logic (HOL) and in Z. Short courses on ProofPower-Z are
available as demand arises.  Information about ProofPower can be
obtained automatically from <[e-mail]>.  Contact
Roger Jones, International Computers Ltd, Eskdale Road, Winnersh,
Wokingham, Berkshire RG11 5TT, UK (tel [phone] ext 6536, fax
[phone], email <[e-mail]> or
<[e-mail]>) for further details.
  Zola is a tool that supports the production and typesetting of Z
specifications, including a type-checker and a Tactical Proof System.
The tool is sold commercially and available to academic users at a
special discount.  For further information, contact K. Ashoo, Imperial
Software Technology, 62-74 Burleigh Street, Cambridge CB1 1DJ, UK (tel
[phone], fax [phone], email <[e-mail]>).
  ZTC is a Z type checker for the PC and Sun available free of charge
via anonymous FTP in compressed Unix tar format under the directory
ise.cs.depaul.edu:/dist (140.192.32.117) and also from the Z archive at
Oxford under the ftp.comlab.ox.ac.uk:/pub/Zforum/ZTC-1.3 directory.  It
is available for educational and non-profit uses and is part of an
ongoing research project developing supporting tools for using Z.
Contact Xiaoping Jia on <[e-mail]> for further information.
  Formaliser is a syntax-directed Z editor and type checker, running
under Microsoft Windows, available from Logica Cambridge.  Contact
Susan Stepney, Logica Cambridge Limited, Betjeman House, 104 Hills Road,
Cambridge CB2 1LQ, UK  (tel [phone], email <[e-mail]>)
for further information.
  DST-fuzz is a set of tools based on the fuzz package by Mike Spivey,
supplying a Motif based user interface for LaTeX based pretty printing,
syntax and type checking. A CASE tool interface allows basic
functionality for combined application of Z together with structured
specifications. The tools are integrated into SoftBench. For further
information contact Hans-Martin Hoercher, DST Deutsche System-Techik
GmbH, Edisonstr. 3, D-24145 Kiel, Germany (tel [phone], fax
[phone], email <[e-mail]>).
  The B-Tool can be used to check proofs concerning parts of Z
specifications.  This is licensed by Edinburgh Portable Compilers Ltd,
17 Alva Street, Edinburgh EH2 4PH, UK (tel [phone], fax
[phone]). Contact the Distribution Manager (email
<[e-mail]>) for further information.
  The B-Toolkit is a set of integrated tools which fully supports the
B-Method for formal software development and is available from B-Core
(UK) Limited, Magdalen Centre, The Oxford Science Park, Oxford OX4 4GA,
UK. For further details, contact Ib Sorensen (tel [phone],
fax [phone], email <[e-mail]>).
  A survey of Z tools may be obtained from Colin Parker, Systems Process
Department, W376C, British Aerospace, Warton Aerodrome, Warton, Preston
PR4 1AX, UK.

Subject: How can I learn about Z?

There are a number of courses on Z run by industry and academia. Oxford
University offers industrial short courses in the use Z.  As well as
introductory courses, recent newly developed material includes advanced
Z-based courses on proof and refinement, partly based around the
B-Tool.  Courses are held in Oxford, or elsewhere (e.g., on a company's
premises) if there is enough demand. For further information, contact
Jim Woodcock (tel [phone], fax [phone], email
<[e-mail]>).
  Logica UK Limited offer a five day course on Z and a three day             |
introductory course on formal methods (mainly Z).  For dates and prices
contact Janet Quickenden [phone] ext 4845.                            |
  Praxis Systems plc runs a range of Z (and other formal methods) courses.
For details contact Anthony Hall on [phone] or <[e-mail]>.
  Formal Systems (Europe) Ltd run a range of Z, CSP and other formal
methods courses, primarily in the US and with such lecturers as Jim
Woodcock and Bill Roscoe (both lecturers at the PRG).  For dates and prices
contact Joy Reed (tel [phone], email <[e-mail]>)
at the PRG or Kate Pearson (tel [phone]) at Formal Systems.
  DST Deutsche System-Technik runs a collection of courses for either Z
or CSP, mainly in Germany. These courses range from half day
introductions to formal methods and Z to one week introductory or
advanced courses, held either at DST, or elsewhere.  For further
information contact Hans-Martin Hoercher, DST Deutsche System-Techik
GmbH, Edisonstr. 3, D-24145 Kiel, Germany (tel [phone], fax
[phone], email <[e-mail]>).

Subject: What has been published about Z?

A compressed BibTeX bibliography of Z-related publications is available
from the PRG archive under ftp.comlab.ox.ac.uk:/pub/Zforum/z.bib.Z (and
ftp.comlab.ox.ac.uk:/pub/Zforum/z.ps.Z in PostScript format).
Information on Oxford University Programming Research Group (PRG)
Technical Monographs and Reports, including many on Z, is available
from the librarian (tel [phone], fax [phone], email
<[e-mail]>).
  "Formal Methods: A Survey" by S.Austin & G.I.Parkin, March 1993
includes information on the use and teaching of Z in industry and
academia.  Contact DITC Office, Formal Methods Survey, National
Laboratory, Teddington, Middlesex TW11 0LW, UK (tel [phone],
fax [phone]) for a copy.
  The following books largely concerning Z have been or are due to be
published (in approximate chronological order):

  I.Hayes (ed.), Specification case studies, Prentice Hall International
      Series in Computer Science, 1987. (2nd ed., 1993)
  J.M.Spivey, Understanding Z: a specification language and its formal
      semantics, Cambridge University Press, 1988.
  D.Ince, An introduction to discrete mathematics, formal system
      specification and Z, Oxford University Press, 1988. (2nd ed., 1993)
  J.C.P.Woodcock & M.Loomes, Software engineering mathematics, Pitman, 1988.
  J.M.Spivey, The Z notation: a reference manual, Prentice Hall
      International Series in Computer Science, 1989. (2nd ed., 1992)
      [Widely used as the current de facto standard for Z.]
  A.Diller, Z: an introduction to formal methods, Wiley, 1990.
  J.E.Nicholls (ed.), Z user workshop, Oxford 1989, Springer-Verlag,
      Workshops in Computing, 1990.
  B.Potter, J.Sinclair & D.Till, An introduction to formal specification
      and Z, Prentice Hall International Series in Computer Science, 1991.
  D.Lightfoot, Formal specification using Z, MacMillan, 1991.
  A.Norcliffe & G.Slater, Mathematics for software construction,
      Ellis Horwood, 1991.
  J.E.Nicholls (ed.), Z user workshop, Oxford 1990, Springer-Verlag,
      Workshops in Computing, 1991.
  I.Craig, The formal specification of advanced AI architectures,
      Ellis Horwood, 1991.
  M.Imperato, An introduction to Z, Chartwell-Bratt, 1991.
  J.B.Wordsworth, Software development with Z, Addison-Wesley, 1992.
  S.Stepney, R.Barden & D.Cooper (eds.), Object orientation in Z,
      Springer-Verlag, Workshops in Computing, August 1992.
  J.E.Nicholls (ed.), Z user workshop, York 1991, Springer-Verlag,
      Workshops in Computing, 1992.
  D.Edmond, Information Modeling: Specification and Implementation,
      Prentice Hall, 1992.
  J.P.Bowen & J.E.Nicholls (eds.), Z user workshop, London 1992,
      Springer-Verlag, Workshops in Computing, 1993.
  S.Stepney, High integrity compilation: A case study, Prentice Hall, 1993.
  M.McMorran & S.Powell, Z guide for beginners, Blackwell Scientific, 1993.
  K.C.Lano & H.Haughton (eds.), Object-oriented specification case studies,
      Prentice Hall International Object-Oriented Series, 1993.
  B.Ratcliff, Introducing Specification Using Z: A Practical Case Study
      Approach, McGraw-Hill, 1994.
  A.Diller, Z: an introduction to formal methods, 2nd ed., Wiley, 1994.
  J.P.Bowen & J.A.Hall (eds.), Z user workshop, Cambridge 1994,
      Springer-Verlag, Workshops in Computing, 1994.
Announced:
  R.Barden, S.Stepney, D.Cooper, Z in practice (A methods handbook for Z),
      Prentice-Hall, 1994 (in press, expected November)                      |
  J.C.P.Woodcock & J.Davies, Using Z: specification, proof and refinement,
      Prentice Hall International Series in Computer Science, 1995?
      (In preparation)

Subject: What is object-oriented Z?

Several object-oriented extensions to or versions of Z have been
proposed.  The book "Object orientation in Z", listed above, is a
collection of papers describing various OOZ approaches - Hall, ZERO,
MooZ, Object-Z, OOZE, Schuman&Pitt, Z++, ZEST and Fresco (an OO VDM
method) - in the main written by the methods' inventors, and all
specifying the same two examples. A more recent book entitled
"Object-oriented specification case studies" surveys the principal
methods and languages for formal object-oriented specification,
including Z-based approaches.

Subject: How can I run Z?

Z is a (non-executable in general) specification language, so there is
no such thing as a Z compiler/linker/etc. as you would expect for a
programming language. Some people have looked at animating subsets of Z
for rapid prototyping purposes, using logic and functional programming
for example, but this work is preliminary and is not really the major
point of Z, which is to increase human understandability of the
specified system and allow the possibility of formal reasoning and
development. However, Prolog seems to be the main favoured language for
Z prototyping and some references may be found in the Z bibliography
(see above).

Subject: Where can I meet other Z people?

The 8th Z User Meeting (ZUM'95) was held on 29-30 June 1994 at St.
John's College, University of Cambridge, UK in association with BCS
FACS.  The 9th Z User Meeting is planned for 7-8 September 1995 in
Limerick, Ireland. For general enquiries, contact the Conference Chair,
Jonathan Bowen (tel [phone], fax [phone], email
<[e-mail]>). Further details will be issued on
comp.specification.z in due course.  The proceedings for Z User
Meetings have been published in the Springer-Verlag Workshops in
Computing series since the 4th meeting in 1989. A Call for Papers for
ZUM'95 is available from http://www.comlab.ox.ac.uk/archive/z/zum95.html
via WWW or ftp.comlab.ox.ac.uk:/pub/Zforum/zum95 via anonymous FTP.
The deadline for paper submissions is 9th December 1994.
  The 6th Refinement Workshop was held at City University, London, UK,
5-7 January 1994. The Programme Chair was David Till, Dept of Computer
Science, City University, Northampton Square, London, EC1V 0HB, UK (tel
[phone], email <[e-mail]>).  The proceedings for
these workshops are currently published in the Springer-Verlag
Workshops in Computing series.
  The first FME (Formal Methods Europe) Symposium was held in Odense,
Denmark, 19-23 April 1993.  The proceedings are available as Springer
LNCS 670. The next FME Symposium will be held 24-28 October 1994 in
Barcelona, Spain.  The Programme Chair is Tim Denvir (tel
[phone], fax [phone], email
<[e-mail]>) and the Organizing Chair in Spain is
Daniel Cabedo (tel [phone], fax [phone], email
<[e-mail]>). The chairman of FME is Martyn Thomas,
Praxis plc, 20 Manvers Street, Bath BA1 1PX, UK (tel [phone],
email <[e-mail]>).
  FORTE addresses formal techniques and testing methodologies
applicable to distributed systems such as Estelle, Lotos, SDL, ASN.1,
Z, etc.  FORTE'93 was held at Boston, Massachusetts, USA on 26-29
October 1993.  The IFIP WG6.1 7th International Conference on Formal
Description Techniques for Distributed Systems and Communications
Protocols will be held at Berne, Switzerland, 4-7 October 1994.  For
further information contact:  FORTE'94 Organization Committee,
University of Berne, PO Box 900, CH-3000 Bern 9, Switzerland (tel
[phone] (Dieter Hogrefe), -4430 (Stefan Leue), fax -3965, email
<[e-mail]>). Additional information is available via
anonymous FTP from the host "siam.unibe.ch" under the directory
"forte94" (see the file "README" first).
  Details of Z-related meetings may be advertized on
  comp.specification.z if desired. All the above meetings are likely to
be repeated in some form.

Subject: What is the Z User Group?

The Z User Group was set up in 1992 to oversee Z-related activities, and
the Z User Meetings in particular.  As a subscriber to comp.specification.z,
ZFORUM or the postal mailing list, you may consider yourself a member
of the Z User Group.  There are currently no charges for membership,
although this is subject to review if necessary.  Contact
<[e-mail]> for further information.

Subject: How can I obtain the draft Z standard?

The proposed Z standard under ISO/IEC JTC1/SC22 is available
electronically via anonymous FTP *only* (not via the mail server since
it is too large) from the Z archive at Oxford in compressed PostScript
format.  Version 1.0 of the draft standard is accessible as the file
ftp.comlab.ox.ac.uk:/pub/Zforum/zstandard1.0.ps.Z together with a annex
in the ftp.comlab.ox.ac.uk:/pub/Zforum/zstandard-annex1.0.ps.Z file.
It is also available in printed form from the Oxford University
Computing Laboratory librarian (tel [phone], fax [phone],
email <[e-mail]>) by requesting Technical Monograph
number PRG-107.

Subject: Where else is Z discussed?

The BCS FACS (British Computer Society Formal Aspects of Computer
Science special interest group) and FME (Formal Methods Europe) are two
organizations interested in formal methods in general. Contact BCS
FACS, Dept of Computer Studies, Loughborough University of Technology,
Loughborough, Leicester LE11 3TU, UK (tel [phone], fax
[phone], email <[e-mail]>) for further information. A
"FACS Europe" newsletter is issued to members of FACS and FME.  Please
send suitable Z-related material to the Z column editor, David Till,
Dept of Computer Science, City University, Northampton Square, London,
EC1V 0HB, UK (tel [phone], email <[e-mail]>) for
possible publication.  Material from articles appearing on the
comp.specification.z newsgroup may be included if considered of
sufficient interest (with permission from the originator if possible).
It would be helpful for posters of articles on comp.specification.z to
indicate if they do not want further distribution for any reason.

Subject: How does VDM compare with Z?

See I.J.Hayes, C.B.Jones & J.E.Nicholls, Understanding the differences
between VDM and Z, FACS Europe, series I, 1(1):7-30, Autumn 1993
available as an on-line Technical Report from Manchester under
ftp.cs.man.ac.uk:/pub/TR/UMCS-93-8-1.ps.Z and I.J.Hayes, VDM and Z: A
comparative case study, Formal Aspects of Computing, 4(1):76-99, 1992.
VDM is discussed on the (unmoderated) VDM FORUM mailing list. Send a
message containing the command "join vdm-forum <name>" where <name> is
your real name to <[e-mail]>. To contact the list
administrator, email John Fitzgerald at the University of Newcastle
upon Tyne, England, on <[e-mail]>.

Subject: What if I have spotted a mistake or an omission?

Please send corrections or new relevant information about meetings,
books, tools, etc., to <[e-mail]>.  New questions
and model answers are also gratefully received!

--
Jonathan Bowen, <[e-mail]>
Programming Research Group, Oxford University Computing Laboratory, UK.